(* # ===================================================================
   # Matrix Project
   # Copyright FEM-NUAA.CN 2020
   # =================================================================== *)


Require Export Matrix.Mat.ZMatrix.
Require Import ZArith.
Require Export Matrix.MMat.MMatrix_Module.
Open Scope Z_scope.

Module ZMMatrix := MMatrix ZM.

Definition ZMMO := ZMMatrix.MMO.

Definition ZMMI := ZMMatrix.MMI.

Definition ZMMeq := @ZMMatrix.MMeq.
Arguments ZMMeq {m}{n}{m2}{n2}.

Definition ZMMadd := @ZMMatrix.MMadd.
Arguments ZMMadd {m0}{n0}{m}{n}.

Definition ZMMopp := @ZMMatrix.MMopp.
Arguments ZMMopp {m0}{n0}{m}{n}.

Definition ZMMsub := @ZMMatrix.MMsub.
Arguments ZMMsub {m0}{n0}{m}{n}.

Definition ZMMmult := @ZMMatrix.MMmult.
Arguments ZMMmult {m}{n}{p}{m2} {n2} {p2}.

Definition ZMMadd_comm:=@ZMMatrix.MMadd_comm.
Definition ZMMadd_assoc:=@ZMMatrix.MMadd_assoc.
Definition ZMMadd_zero_l:=@ZMMatrix.MMadd_zero_l.
Definition ZMMadd_zero_r:=@ZMMatrix.MMadd_zero_r.

Definition ZMMsub_opp:=@ZMMatrix.MMsub_opp.
Definition ZMMsub_assoc:=@ZMMatrix.MMsub_assoc.
Definition ZMMsub_zero_l:=@ZMMatrix.MMsub_zero_l.
Definition ZMMsub_zero_r:=@ZMMatrix.MMsub_zero_r.
Definition ZMMsub_self:=@ZMMatrix.MMsub_self.

Definition ZMMmul_add_distr_l:= @ZMMatrix.MMmul_add_distr_l.
Definition ZMMmul_add_distr_r:= @ZMMatrix.MMmul_add_distr_r.
Definition ZMMmul_sub_distr_l:= @ZMMatrix.MMmul_sub_distr_l.
Definition ZMMmul_sub_distr_r:= @ZMMatrix.MMmul_sub_distr_r.
Definition ZMMmul_assoc:= @ZMMatrix.MMmul_assoc.
Definition ZMMmul_zero_l := @ZMMatrix.MMmul_zero_l.
Definition ZMMmul_zero_r := @ZMMatrix.MMmul_zero_r.

Definition ZMMtteq:= @ZMMatrix.MMtteq.
Definition ZMMtrans_add:= @ZMMatrix.MMtrans_add.
Definition ZMMtrans_sub:= @ZMMatrix.MMtrans_sub.
Definition ZMMtrans_mul:= @ZMMatrix.MMtrans_mul.




